Nuprl Lemma : R-implies-rule 11,40
A:es_realizer{i:l}, P,Q:(event_system{i:l}prop{i':l}).
R-realizes{i:l}
R-realizes(A; es.P(es))
 (es:event_system{i:l}. P(es)  Q(es))
 R-realizes{i:l}
 R-realizes(A; es.Q(es)) 
latex

Definitionst  T, P  Q, x(s), R-realizes{i:l}(R; es.P(es)), P  Q, prop{i:l}, x:A. B(x)
Lemmases realizer wf, R-Feasible wf, event system wf, R-consistent wf

origin